/*
 * UnaryClausesRemover.cuh
 *
 *  Created on: Sep 4, 2013
 *      Author: jaime
 */

#ifndef UNARYCLAUSESREMOVER_CUH_
#define UNARYCLAUSESREMOVER_CUH_

#include <vector>
#include "../SATSolver/SolverTypes.cuh"
#include <assert.h>
#include "../SATSolver/SATSolver.cuh"

using namespace std;

class UnaryClausesRemover {
private:
	vector<Clause> * formula_host;
	vector<Lit> set_literals;
	sat_status status;
	int number_of_variables;

	bool add(Lit literal);
	sat_status process_clause(std::vector<Lit> & implied_lits, Clause c, Lit & unit_lit);
	void clean_clause(std::vector<Lit> & implied_lits, Clause & c);

public:
	UnaryClausesRemover(vector<Clause> * formula_host, int number_of_variables);
	void process_unary_clauses();
	void propagate_literals();
	void process();
	sat_status get_status();
	/**
	 * Adds the current set literals to 'literals'
	 */
	void get_set_literals(vector< Lit > & literals);

	// Test method
	void print_set_literals();
	void print_host_formula();
	bool test_results();
};

#endif /* UNARYCLAUSESREMOVER_CUH_ */
